We observe that the various formulations of the operational semantics ofConstraint Handling Rules proposed over the years fall into a spectrum rangingfrom the analytical to the pragmatic. While existing analytical formulationsfacilitate program analysis and formal proofs of program properties, theycannot be implemented as is. We propose a novel operational semantics, whichhas a strong analytical foundation, while featuring a terminating executionmodel. We prove its soundness and completeness with respect to existinganalytical formulations and we provide an implementation in the form of asource-to-source transformation to CHR with rule priorities.
展开▼
